RCS "$Id: Logic2Protected.sig,v 1.7 1998/08/13 11:38:49 pxs Exp $";
(* Another logic used internally by the CWB, e.g. in model-checking          *)
(* All variables must be bound, and they must be distinct.                   *)
(* (This is assured by the translator.)                                      *)

signature LOGIC2_PROTECTED =
sig
  structure M : MODALITY_PROTECTED
   datatype privateProp = True
    | False
    | Var of int
    | And of prop * prop
    | Or of prop * prop
    | Nec of M.modality * prop
    | Pos of M.modality * prop
    | Max of int * prop
    | Min of int * prop
    and prop = DUMMY of (privateProp * word) ref

   val printString : prop -> string
     
   val real : prop -> privateProp
   val makeProp : privateProp -> prop

   val hashval : prop -> word
   val le : prop * prop -> bool

   (* Accept a list of user-chosen variable names in order, corresponding*)
   (* with the integers in a prop. Perdita, better way? *)
   val varNameList : string list -> unit

end

